\footnotesize{
\begin{verbatim}

%%%%% Declaración de variables: %%%%%

var 1..5: board_id_0;
var 1..5: board_id_1;
var 1..5: board_x_0;
var 1..5: board_x_1;
var 1..5: board_y_0;
var 1..5: board_y_1;
var 1..5: player_id_0;
var 1..5: player_id_1;

%%%%% Definición de restricciones: %%%%%

constraint ((((true /\ (true /\ (player_id_0 != player_id_1))) /\ true) 
/\ ((((((true /\ (true /\ (player_id_0 != player_id_1))) /\ true) /\ 
((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\ 
(true /\ ((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) 
/\ (board_id_0 = player_id_0)) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1)
\/ (board_y_0 != board_y_1)))) /\ true)) /\ (board_id_1 = player_id_0)))) /\
(player_id_0 = player_id_0)) \/ ((((true /\ (true /\ (player_id_0 != player_id_1)))
/\ true) /\ ((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\ (true /\
((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) /\ 
(board_id_0 = player_id_1)) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) 
\/ (board_y_0 != board_y_1)))) /\ true)) /\ (board_id_1 = player_id_1)))) /\ 
(player_id_1 = player_id_0))) /\ (not ((((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) \/ 
(board_y_0 != board_y_1)))) /\ true)) /\ ((board_id_0 = player_id_0) /\ 
(not ((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\ (true /\ 
((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) /\ 
((((board_x_0 - board_x_0) * (board_y_0 - board_y_0)) = 0) /\ 
(board_id_0 != board_id_0))) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) \/ 
(board_y_0 != board_y_1)))) /\ true)) /\ 
((((board_x_1 - board_x_0) * (board_y_1 - board_y_0)) = 0) /\
(board_id_0 != board_id_1))))))) \/ (((((board_id_0 = player_id_0) \/
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) \/
(board_y_0 != board_y_1)))) /\ true)) /\ ((board_id_1 = player_id_0) /\ 
(not ((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\ 
(true /\ ((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) /\
((((board_x_0 - board_x_1) * (board_y_0 - board_y_1)) = 0) /\ 
(board_id_1 != board_id_0))) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1)
\/ (board_y_0 != board_y_1)))) /\ true)) /\ 
((((board_x_1 - board_x_1) * (board_y_1 - board_y_1)) = 0) /\ 
(board_id_1 != board_id_1))))))))))) \/ (((true /\ (true /\ 
(player_id_0 != player_id_1))) /\ true) /\ ((((((true /\ (true /\ 
(player_id_0 != player_id_1))) /\ true) /\ ((((((board_id_0 = player_id_0)
\/ (board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1)
\/ (board_y_0 != board_y_1)))) /\ true)) /\ (board_id_0 = player_id_0)) \/ 
(((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\
(true /\ ((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true))
/\ (board_id_1 = player_id_0)))) /\ (player_id_0 = player_id_1)) \/ 
((((true /\ (true /\ (player_id_0 != player_id_1))) /\ true) /\ 
((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\ (true /\ 
((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) /\ 
(board_id_0 = player_id_1)) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) \/ 
(board_y_0 != board_y_1)))) /\ true)) /\ (board_id_1 = player_id_1)))) /\ 
(player_id_1 = player_id_1))) /\ (not ((((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) \/ 
(board_y_0 != board_y_1)))) /\ true)) /\ ((board_id_0 = player_id_1) /\ 
(not ((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\ 
(true /\ ((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) /\
((((board_x_0 - board_x_0) * (board_y_0 - board_y_0)) = 0) /\ 
(board_id_0 != board_id_0))) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1)
\/ (board_y_0 != board_y_1)))) /\ true)) /\ 
((((board_x_1 - board_x_0) * (board_y_1 - board_y_0)) = 0) /\ 
(board_id_0 != board_id_1))))))) \/ (((((board_id_0 = player_id_0) \/
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1)
\/ (board_y_0 != board_y_1)))) /\ true)) /\ ((board_id_1 = player_id_1) /\ 
(not ((((((board_id_0 = player_id_0) \/ (board_id_0 = player_id_1)) /\ 
((board_id_1 = player_id_0) \/ (board_id_1 = player_id_1))) /\ ((true /\
(true /\ ((board_x_0 != board_x_1) \/ (board_y_0 != board_y_1)))) /\ true)) /\ 
((((board_x_0 - board_x_1) * (board_y_0 - board_y_1)) = 0) /\ 
(board_id_1 != board_id_0))) \/ (((((board_id_0 = player_id_0) \/ 
(board_id_0 = player_id_1)) /\ ((board_id_1 = player_id_0) \/ 
(board_id_1 = player_id_1))) /\ ((true /\ (true /\ ((board_x_0 != board_x_1) \/
(board_y_0 != board_y_1)))) /\ true)) /\ 
((((board_x_1 - board_x_1) * (board_y_1 - board_y_1)) = 0) /\ 
(board_id_1 != board_id_1))))))))))));

%%%%% Llamada al resolutor: %%%%%

solve satisfy;

%%%%% Formato de salida: %%%%%

output [" INSERT INTO board (id,x,y) VALUES (", show(board_id_0),",", 
show(board_x_0),",", show(board_y_0),");"," INSERT INTO board (id,x,y)
 VALUES (", show(board_id_1),",", show(board_x_1),",", show(board_y_1),
");"," INSERT INTO player (id) VALUES (", show(player_id_0),");"," 
INSERT INTO player (id) VALUES (", show(player_id_1),");"];
\end{verbatim}
}